(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x5eaa93db416daeca) #xbd5527b682db5d95))
(constraint (= (f #x8c423e6e8470bc32) #x8c423e6e8470bc31))
(constraint (= (f #x9c6e685bc7b51e88) #x38dcd0b78f6a3d11))
(constraint (= (f #x0e7e7cebe41acc9b) #x1cfcf9d7c8359937))
(constraint (= (f #x6171ec4a5b41c87c) #x6171ec4a5b41c87b))
(constraint (= (f #x6c8589d1e5c76e3e) #x6c8589d1e5c76e3d))
(constraint (= (f #xec48626bd2ec9b29) #xec48626bd2ec9b28))
(constraint (= (f #xea56eeb012d5e4c2) #xd4addd6025abc985))
(constraint (= (f #x54b487953da65a79) #x54b487953da65a78))
(constraint (= (f #x6ee38462770b2e08) #xddc708c4ee165c11))
(constraint (= (f #x91ed897e8ce3b534) #x91ed897e8ce3b533))
(constraint (= (f #xd4bc109959e41e10) #xa9782132b3c83c21))
(constraint (= (f #x1d725ed5352e5667) #x1d725ed5352e5666))
(constraint (= (f #x4996cb29ade107ba) #x4996cb29ade107b9))
(constraint (= (f #x677da0edc9156eeb) #x677da0edc9156eea))
(constraint (= (f #x247ae5dd102354e8) #x247ae5dd102354e7))
(constraint (= (f #x229779b0eb5134b2) #x229779b0eb5134b1))
(constraint (= (f #x99e6224ea83e7102) #x33cc449d507ce205))
(constraint (= (f #x030391d72e948b0e) #x060723ae5d29161d))
(constraint (= (f #xdea4160a37867be5) #xdea4160a37867be4))
(constraint (= (f #x463325ce73de5de1) #x463325ce73de5de0))
(constraint (= (f #xcc0c2ce36382ed08) #x981859c6c705da11))
(constraint (= (f #xe5c2dee882eb05eb) #xe5c2dee882eb05ea))
(constraint (= (f #x6eb6e2459ee33b13) #xdd6dc48b3dc67627))
(constraint (= (f #x4054a952a4dbb078) #x4054a952a4dbb077))
(constraint (= (f #xcbac2162d854d406) #x975842c5b0a9a80d))
(constraint (= (f #x4a3dddb0d8ea8d54) #x947bbb61b1d51aa9))
(constraint (= (f #x43bc8c14689eb037) #x43bc8c14689eb036))
(constraint (= (f #x4ac7424b1944b92c) #x4ac7424b1944b92b))
(constraint (= (f #xea2c4b953505b262) #xea2c4b953505b261))
(constraint (= (f #x4bd24e0e6eeee96c) #x4bd24e0e6eeee96b))
(constraint (= (f #xa8b7e3cee78d07e3) #xa8b7e3cee78d07e2))
(constraint (= (f #x49b2acedebcd4b27) #x49b2acedebcd4b26))
(constraint (= (f #x47d77b391a4bb614) #x8faef67234976c29))
(constraint (= (f #x195de65e59dc5028) #x195de65e59dc5027))
(constraint (= (f #x99404a46a88ac276) #x99404a46a88ac275))
(constraint (= (f #x123d9a27d99b3b4c) #x247b344fb3367699))
(constraint (= (f #x4028a17dce64e428) #x4028a17dce64e427))
(constraint (= (f #xb24656c1d99708e1) #xb24656c1d99708e0))
(constraint (= (f #xe033b4ee1262ce8e) #xc06769dc24c59d1d))
(constraint (= (f #x197b1dc15c5aedea) #x197b1dc15c5aede9))
(constraint (= (f #xd18877d8a62ebc8e) #xa310efb14c5d791d))
(constraint (= (f #xe2375aebc6e2be16) #xc46eb5d78dc57c2d))
(constraint (= (f #x1ae48e3b696951d5) #x35c91c76d2d2a3ab))
(constraint (= (f #x25cc0b338ec0e116) #x4b9816671d81c22d))
(constraint (= (f #xe40cdae268a61e81) #xc819b5c4d14c3d03))
(constraint (= (f #x1c4ab118c6c49dea) #x1c4ab118c6c49de9))
(constraint (= (f #x31a23cc6c1e4a1d2) #x6344798d83c943a5))
(constraint (= (f #x26dd6140c77ae756) #x4dbac2818ef5cead))
(constraint (= (f #xa798c5c38d17ec44) #x4f318b871a2fd889))
(constraint (= (f #xee58e1b794d09c09) #xdcb1c36f29a13813))
(constraint (= (f #x5e6d06e85be2db7a) #x5e6d06e85be2db79))
(constraint (= (f #x494351e3eb20a581) #x9286a3c7d6414b03))
(constraint (= (f #xe054875e528094e5) #xe054875e528094e4))
(constraint (= (f #x43b306b82791b898) #x87660d704f237131))
(constraint (= (f #xe64adad02b8c1115) #xcc95b5a05718222b))
(constraint (= (f #x5e60bba3661d27c7) #xbcc17746cc3a4f8f))
(constraint (= (f #x00ac04e91e7258a2) #x00ac04e91e7258a1))
(constraint (= (f #xe0b31e52ce150549) #xc1663ca59c2a0a93))
(constraint (= (f #x8e3992bb3c059e5b) #x1c732576780b3cb7))
(constraint (= (f #xb088a4edeac46ce8) #xb088a4edeac46ce7))
(constraint (= (f #x57953d0cb5e26c7e) #x57953d0cb5e26c7d))
(constraint (= (f #x09b0536112e81b91) #x1360a6c225d03723))
(constraint (= (f #x6bc14a1ac4241ec3) #xd782943588483d87))
(constraint (= (f #xadedebc9398a7aee) #xadedebc9398a7aed))
(constraint (= (f #xe02be708e3cde6a5) #xe02be708e3cde6a4))
(constraint (= (f #x169b4a25da740406) #x2d36944bb4e8080d))
(constraint (= (f #xd17c4195a593dc54) #xa2f8832b4b27b8a9))
(constraint (= (f #x72baee7b3a4923d5) #xe575dcf6749247ab))
(constraint (= (f #x126a9beab04132eb) #x126a9beab04132ea))
(constraint (= (f #xaa27bc7e8ebe38db) #x544f78fd1d7c71b7))
(constraint (= (f #x621eb21e55a52ea7) #x621eb21e55a52ea6))
(constraint (= (f #x0c0e23b09cce0c3e) #x0c0e23b09cce0c3d))
(constraint (= (f #x6541e564a9ca2c74) #x6541e564a9ca2c73))
(constraint (= (f #xdc6ead966347a127) #xdc6ead966347a126))
(constraint (= (f #xbccee17ac54e6c17) #x799dc2f58a9cd82f))
(constraint (= (f #x937220a22a5e24e0) #x937220a22a5e24df))
(constraint (= (f #x5ee5432621eb2640) #xbdca864c43d64c81))
(constraint (= (f #x370e8363d88b02e6) #x370e8363d88b02e5))
(constraint (= (f #x80ec73e89558cde4) #x80ec73e89558cde3))
(constraint (= (f #x1e84a915de0135ee) #x1e84a915de0135ed))
(constraint (= (f #x1a33ebd7b399585e) #x3467d7af6732b0bd))
(constraint (= (f #xa2e875493e5c5cae) #xa2e875493e5c5cad))
(constraint (= (f #xe56324ea1a681e56) #xcac649d434d03cad))
(constraint (= (f #x0db5de19363b3762) #x0db5de19363b3761))
(constraint (= (f #xb8ee373d5615ba89) #x71dc6e7aac2b7513))
(constraint (= (f #xb2a1228823a0456c) #xb2a1228823a0456b))
(constraint (= (f #x91c260ce63b31371) #x91c260ce63b31370))
(constraint (= (f #x2eb5289b238203ac) #x2eb5289b238203ab))
(constraint (= (f #xa8c94dcc5e728674) #xa8c94dcc5e728673))
(constraint (= (f #x9003cebb03b394e4) #x9003cebb03b394e3))
(constraint (= (f #xc25ae68e9be466e0) #xc25ae68e9be466df))
(constraint (= (f #x52ed4c48b96dea97) #xa5da989172dbd52f))
(constraint (= (f #x42c2ee94b11c4e61) #x42c2ee94b11c4e60))
(constraint (= (f #x4d484e5ae2e62ee5) #x4d484e5ae2e62ee4))
(constraint (= (f #xda07ed6d78374eeb) #xda07ed6d78374eea))
(constraint (= (f #x9edce7419717e3aa) #x9edce7419717e3a9))
(constraint (= (f #x9e6d9c3a71a11d34) #x9e6d9c3a71a11d33))
(constraint (= (f #x3420ad3a2cad7622) #x3420ad3a2cad7621))
(constraint (= (f #x6ac892dde6ec6634) #x6ac892dde6ec6633))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvsrem x #x000000000000000b) #x0000000000000000) (ite (= (bvor #x0000000000000003 x) x) (bvnot (bvneg x)) (ite (= (bvor #x0000000000000010 x) x) (bvsub x (bvnot x)) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvnot (bvneg x)) (ite (= (bvand #x0000000000000007 x) #x0000000000000000) (ite (= (bvsrem x #x000000000000000a) #x0000000000000000) (bvsub x (bvnot x)) (bvnot (bvneg x))) (bvsub x (bvnot x)))))) (ite (= (bvsrem x #x000000000000000a) #x0000000000000000) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (ite (= (bvor #x0000000000000008 x) x) (bvsub x (bvnot x)) (bvnot (bvneg x))) (bvnot (bvneg x))) (ite (= (bvurem x #x000000000000000a) #x0000000000000000) (bvnot (bvneg x)) (ite (= (bvurem x #x0000000000000009) #x0000000000000001) (ite (= (bvor #x000000000000000e x) x) (ite (= (bvashr x x) #x0000000000000000) (bvnot (bvneg x)) (bvsub x (bvnot x))) (bvnot (bvneg x))) (ite (= (bvor #x0000000000000010 x) x) (ite (= (bvurem x #x000000000000000b) #x0000000000000001) (bvnot (bvneg x)) (ite (= (bvashr x x) #x0000000000000000) (ite (= (bvand #x000000000000000b x) #x0000000000000001) (bvsub x (bvnot x)) (ite (= (bvand #x0000000000000005 x) #x0000000000000000) (ite (= (bvand #x0000000000000007 x) #x0000000000000000) (bvsub x (bvnot x)) (bvnot (bvneg x))) (ite (= (bvand #x0000000000000003 x) #x0000000000000001) (bvnot (bvneg x)) (ite (= (bvurem x #x000000000000000c) #x0000000000000000) (bvnot (bvneg x)) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvand #x0000000000000009 x) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvand #x0000000000000004 x) #x0000000000000000) (bvsub x (bvnot x)) (bvnot (bvneg x))))))))) (bvsub x (bvnot x)))) (ite (= (bvand #x0000000000000007 x) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvurem x #x0000000000000005) #x0000000000000001) (bvnot (bvneg x)) (ite (= (bvor #x0000000000000005 x) x) (ite (= (bvsrem x #x0000000000000003) #x0000000000000000) (ite (= (bvor #x0000000000000003 x) x) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvnot (bvneg x)) (bvsub x (bvnot x))) (bvnot (bvneg x))) (bvnot (bvneg x))) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvsub x (bvnot x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) (ite (= (bvor #x0000000000000003 x) x) (bvnot (bvneg x)) (bvsub x (bvnot x))) (ite (= (bvor #x0000000000000006 x) x) (ite (= (bvashr x x) #x0000000000000000) (bvsub x (bvnot x)) (bvnot (bvneg x))) (ite (= (bvashr x x) #x0000000000000000) (bvnot (bvneg x)) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvurem x #x0000000000000009) #x0000000000000000) (ite (= (bvor #x0000000000000008 x) x) (bvnot (bvneg x)) (bvsub x (bvnot x))) (bvnot (bvneg x))) (bvsub x (bvnot x))))))))))))))))
